(* $Id: unifier.ml 185 2008-02-06 16:24:22Z yann.regisgianas $ *)

(** This module implements unification of (ranked) multi-equations
    over a row algebra, that is, an algebra obtained by extending a
    free algebra [A] with rows.

    For the purposes of this module, a rank is an element of an
    arbitrary total order. A rank is associated with every
    multi-equation. When two multi-equations are merged, the smaller
    rank is kept.

    It is understood that finite and infinite terms are legal -- no
    occur check is performed here. *)

open Misc
open Position
type position = Position.t
open CoreAlgebra
open MultiEquation

(** This module implements unification of (ranked) multi-equations
    over a row algebra, that is, an algebra obtained by extending a
    free algebra [A] with rows (see module {!CoreAlgebra}).

    It is understood that finite and infinite terms are legal -- no
    occur check is performed here. 

    This module is purely functional. Thus, backtracking is facilitated:
    the client can define a backtracking behavior on local error.

*)

open Position
open MultiEquation
open CoreAlgebra

(** Types are first-order terms whose variables are picked into a set of
    multi-equations. *)
type typ = variable term

module Make 
  (Context : 
    sig
      type definition
      type description
      type context

      type multi_equation = (definition, description, context) MultiEquation.t

      (** [merge_variables e u v1 v2] is called to merge the description
	  of the multi-equations of [v1] and [v2]. *)
      val merge_variables : 
	multi_equation -> variable -> variable -> multi_equation

      (** [fresh_variable e v1 v2] is called to obtain a fresh variable
	  with respect to [e] when [v1] and [v2] are about to be unified. *)
      val fresh_variable : 
	multi_equation -> variable -> variable -> variable * multi_equation

      (** [variable_structure e v] returns an optional first order 
	  term which is equal to [v] in [e]. *)
      val variable_structure : multi_equation -> variable -> typ option

      (** [eq_variable_structure e v t] adds the equation [v = t] in [e]. *)
      val eq_variable_structure : 
	multi_equation -> variable -> typ -> multi_equation

      exception Error

      type backtrace

      (** [no_hope b] equals true when backtracking is not necessary. *)
      val no_hope : backtrace -> bool

      (** The backtrack function is called when an error occurs. The
	  unifier pop its stack and [backtrack] is called at each
	  parent unification problem to build a [backtrace] or to
	  resume the unification with a new problem. If [no_hope backtrace]
	  is true, then the backtracking is stopped and a unification
	  exception is thrown for the global unification problem with
	  the local unification error. *)
      val backtrack : multi_equation -> variable -> variable -> backtrace 
	-> (multi_equation * variable * variable, backtrace) Misc.choice

    end) =
struct

  open Context

  exception UnificationError of backtrace * multi_equation * variable * variable
  exception LocalError of backtrace

  (** [unify e v1 v2] equates the variable [v1] and [v2] of the system of 
      equations [e]. 
      
      It rewrites the system of equations in a number of ways until an
      inconsistency is found or a standard (satisfiable) form is
      reached. In the former case, a backtracking function is processed
      locally. In the latter case, the function returns normally the
      resulting [e]. *)
  
  let unify e v1 v2 =
    
    (* Define an auxiliary function which creates a fresh variable,
       found within a multi-equation of its own. Its structure is
       given . *)
    
    let fresh e v1 v2 structure =
      let (v, e) = fresh_variable e v1 v2 in
      let e = match structure with 
	| None -> e
	| Some structure -> eq_variable_structure e v structure 
      in
	(v, e)
    in

    let rec unify e v1 v2 = 
      
      let merge_variables e v1 v2 =
	try
	  merge_variables e v1 v2
	with LocalError backtrace -> 
	  if no_hope backtrace then 
	    raise (UnificationError (backtrace, e, v1, v2))
	  else 
	    match backtrack e v1 v2 backtrace with
	      | Left (e, v1, v2) -> unify e v1 v2
	      | Right backtrace -> raise (LocalError backtrace)
      in

      (* If the two variables already belong to the same multi-equation,
	 there is nothing to do. This check is not just an optimization;
	 it is essential in guaranteeing termination, since we are
	 dealing with potentially cyclic structures. *)
      
      if not (MultiEquation.equivalent e v1 v2) then
	
	(* Before performing a recursive call, we will merge the
	   multi-equations associated with [v1] and [v2]. *)
	
	let fresh e = fresh e v1 v2 in
	let merge e = merge_variables e v1 v2 in
	let merge' e s = 
	  let e = merge_variables e v1 v2 in 
	    match s with 
	      | None -> e
	      | Some s -> eq_variable_structure e v1 s
	in
	  (* Another auxiliary function, for syntactic convenience. *)
	  
	let filter e v term =
	  let (v', e) = fresh e (Some term) in
	    unify e v v' 
	in

	  (* Now, let us look at the structure of the two multi-equations. *)

	  match variable_structure e v1, variable_structure e v2 with

	      (* Neither multi-equation contains a term. 
		 Merge them; we're done. *)

	    | None, None ->
		merge e 

		  (* Exactly one multi-equation contains a term; keep it. *)

	    | None, t | t, None ->
		merge' e t

		  (* An intermediate variable can be removed. *)

	    | Some (Var v), _ ->
		unify e v v2
		  
	    | _, Some (Var v) ->
		unify e v v1

		  (* Both multi-equations contain terms whose head symbol belong
		     to the free algebra [A]. Merge the multi-equations
		     (dropping one of the terms), then decompose the equation
		     that arises between the two terms. Signal an error if the
		     terms are incompatible, i.e. do not have the same head
		     symbol. *)

	    | Some (App (term1, term2)), Some (App (term1', term2')) ->
		let e = merge e in
		let e = unify e term1 term1' in
		  unify e term2 term2'

		    (* Both multi-equations contain a uniform row term. 
		       Merge the multi-equations (dropping one of the terms), 
		       then decompose the equation that arises between 
		       the two terms. *)

	    | Some (RowUniform content1), Some (RowUniform content2) ->
		let e = merge e in
		  unify e content1 content2

		    (* Both multi-equations contain a ``row cons'' term. 
		       Compare their labels. *)

	    | ((Some (RowCons (label1, hd1, tl1))) as t1),
		((Some (RowCons (label2, hd2, tl2))) as t2) ->
		let c = RowLabel.compare label1 label2 in
		  if c = 0 then begin

		    (* The labels coincide. This is the cheapest
		       case. Proceed as in the case of free terms above. *)

		    let e = merge e in
		    let e = unify e hd1 hd2 in
		      unify e tl1 tl2

		  end
		  else begin

		    (* The labels do not coincide. We must choose which
		       descriptor (i.e. which term) to keep. We choose to
		       keep the one that exhibits the smallest label
		       (according to an arbitrary, fixed total order on
		       labels). This strategy favors a canonical
		       representation of rows, where smaller labels come
		       first. This should tend to make the cheap case above
		       more frequent, thus allowing rows to be unified in
		       quasi-linear time. *)

		    let e = if c < 0 then merge' e t1 else merge' e t2 in
		      
		      (* Decompose the equation that arises between the two
			 terms. We must create an auxiliary row variable, as
			 well as two auxiliary row terms. Because their value
			 is logically determined by that of [v1] or [v2], it
			 is appropriate to give them the same rank. *)
		      
		    let (tl, e) = fresh e None in
		    let e = filter e tl1 (RowCons (label2, hd2, tl)) in
		      filter e tl2 (RowCons (label1, hd1, tl))

		  end

		    (* The left-hand multi-equation contains a ``row cons'' 
		       term, while the right-hand one contains a ``free'' 
		       term; or the converse. *)

	    | Some (RowCons (label1, hd1, tl1)), 
		  Some (App (term, term'))

	    | Some (App (term, term')), 
		  Some (RowCons (label1, hd1, tl1)) ->

		let attach e son = 
		  let (hd, e) = fresh e None in
		  let (tl, e) = fresh e None  in
		  let e = filter e son (RowCons (label1, hd, tl)) in 
		    ((hd, tl), e)
		in
		let ((hd, tl), e) = attach e term in
		let ((hd', tl'), e) = attach e term' in
		let e = filter e hd1 (App (hd, hd')) in
		  filter e tl1 (App (tl, tl'))

		    (* The left-hand multi-equation contains a ``free'' term,
		       while the right-hand one contains a uniform row term; or
		       the converse. *)

	    | (Some (RowUniform content2) as t), (Some (App (term2, term2'))) 
	    | Some (App (term2, term2')), (Some (RowUniform content2) as t) ->

		let e = merge' e t in
		let attach e son =
		  let (content, e) = fresh e None in 
		  let e = filter e son (RowUniform content) in
		    (content, e)
		in
		let (term2, e) = attach e term2 in
		let (term2', e) = attach e term2' in
		let content1 = App (term2, term2')
		in
		  filter e content2 content1

	    | Some (RowCons (label1, hd1, tl1)), 
		(Some (RowUniform content2) as t)

	    | (Some (RowUniform content2) as t), 
		Some (RowCons (label1, hd1, tl1)) ->

		(* Keep the uniform representation, which is more compact. *)

		let e = merge' e t in

		  (* Decompose the equation that arises between the two
		     terms. To do so, equate [hd1] with [content2], then
		     equate [tl1] with a fresh uniform row whose content is
		     [content2].

		     Note that, instead of creating the latter fresh, one
		     may wish to re-use [v2], which is also a uniform row
		     whose content is [content2]. However, these two terms
		     do not have the same sort. Although this optimization
		     would most likely be correct, its proof of correctness
		     would be more involved, requiring a single variable to
		     simultaneously possess several sorts. *)

		let e = unify e hd1 content2 in
		  filter e tl1 (RowUniform content2)
      else 
	e
    in 
      unify e v1 v2

end
